(declare-const i12 Int)
(declare-const Str3 String)
(declare-const Str11 String)
(declare-const Str12 String)
(declare-const Str19 String)
(assert (>= (str.len Str12) 308))
(push)
(assert (>= (str.len Str19) 37))
(assert (or (= Str11 (str.++ Str12 "" Str3 Str19) (str.++ Str12 "" Str3 Str19) (str.++ Str3 Str3)) (= Str11 Str12 "" "")))
(check-sat)
